COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	facts about sets of integers
C00003 00003	basic set-theoretic notions
C00010 00004	more induction
C00012 00005	max and min of objects
C00014 00006	sets on natural numbers and the order relation
C00018 ENDMK
C⊗;
;facts about sets of integers

(wipe-out)
(get-proofs natnum prf ekl sys)
;basic set-theoretic notions
;6s
(proof set)

(decl (f funct) (type: |ground→ground|))
(decl (rel) (type: |ground⊗ground→truthval|))
(decl univ (type: |@set|))
(define univ |∀n.univ(n)=true|)
(label simpinfo) (label univdef)

(decl intersection (type: |@set⊗@set→@set|)
      (infixname: ∩) (bindingpower: 950) (prefixname: intersection))
(define intersection |∀a b.a∩b=λxv.(a(xv)∧b(xv))|)
(label interdef)

(decl union (type: |@set⊗@set→@set|)
      (infixname: ∪) (bindingpower: 950) (prefixname: union))
(define union |∀a b.a∪b=λxv.(a(xv)∨b(xv))|)
(label uniondef)

(decl inclusion (type: |@set⊗@set→truthval|)
      (infixname: ⊂) (bindingpower: 920) (prefixname: inclusion))
(define inclusion |∀a b.a⊂b≡∀n.a(n)⊃b(n)|)
(label inclusiondef)

(decl inverse (type: |@funct⊗@set⊗ground→@set|))
(define inverse |∀f a n.inverse(f,a,n)=λxv.(a(xv)∧f(xv)=n)|)
(label inversedef)

(trw |∀f a n.inverse(f,a,n)⊂a| (open inverse inclusion))
;∀f a n.inverse(f,a,n)⊂a
(label simpinfo)
(label inverseprop)

(trw |∀f a.(∀n.f(n)=0∨f(n)=1)⊃a⊂(inverse(f,a,0)∪inverse(f,a,1))|
     (open inverse inclusion union))
;∀f a.(∀n.f(n)=0∨f(n)=1)⊃a⊂(inverse(f,a,0)∪inverse(f,a,1))
(label simpinfo)
(label inverseprop1)

(decl epsilon (type: |ground⊗@set→truthval|) (infixname: ε) (bindingpower: 925))
(define epsilon |∀a n.nεa≡a(n)|)
(label epsilondef)

(decl transitive (type: |@rel→truthval|))
(define transitive
	|∀rel.transitive(rel)≡(∀n m k.rel(n,m)∧rel(m,k)⊃rel(n,k))|)
(label transdef)
 
(decl segm (type: |ground→@set|))
(define segm |∀n.segm(n)=(λxv.xv<n)|)
(label segmdef)

(decl tail (type: |ground→@set|))
(define tail |∀n.tail(n)=(λxv.n<xv)|)
(label taildef)
;more induction

(proof induction)

(decl iniset (type: |@set|))
(decl setseq (type: |ground→@set|))
(decl indsclause (type: |@set⊗ground→@set|))

(axiom
 |∀iniset indsclause.∃setseq.setseq(0)=iniset∧
                             (∀n.setseq(n')=indsclause(setseq(n),n))|)
(label inductive_set_definition)

(axiom |∀rel.transitive(rel)∧(∀n.rel(n,n'))⊃(∀n m.n<m⊃rel(n,m))|)
(label transitive_induction)

(axiom |∀indcclause.∃a.∀n.a(n)≡indcclause(a∩segm(n),n)|)
(label course_of_values_definition)
;max and min of objects

(proof minmax)

(decl max (type: |((ground⊗ground)∨(ground→truthval))→ground|) (syntype: constant))

(decl min (type: |((ground⊗ground)∨(ground→truthval))→ground|) (syntype: constant))

(axiom |∀n m.natnum(min(n,m))|)
(label simpinfo)

(axiom |∀n m.natnum(max(n,m))|)
(label simpinfo)

(axiom |∀n m k.k<max(n,m)≡k<n∨k<m|)
(label maxdef)

(axiom |∀n m k.k<min(n,m)≡k<n∧k<m|)
(label mindef)

(axiom |∀a.natnum max a|)
(label simpinfo)

(axiom |∀a.natnum min a|)
(label simpinfo)

(axiom |∀a.(∃n.a(n))⊃a(min(a))|)
(label minprop)
 
(axiom |∀a ∀n.n<min(a)⊃¬a(n)|)
(label minprop1)
 
(trw |∀a.(∃n.a(n))≡a(min(a))| (der minprop))
(label minprop2)
;sets on natural numbers and the order relation
(proof unbound)
;7s

(decl unbound (type: |@set→truthval|))
(define unbound |∀a.unbound(a)≡(¬∃n.a⊂segm(n))|)
(label simpinfo) (label unboundef)
 
(trw |unbound(univ)| (open unbound inclusion segm) (der irreflexivity_of_order))
;UNBOUND(UNIV)
(label simpinfo)

;the basic splitting property

(trw |∀a b c.(a⊂b∪c∧unbound(a)⊃(unbound(b)∨unbound(c)))|
     (open unbound inclusion segm union) (der maxdef))
;∀A B C.A⊂B∪C∧UNBOUND(A)⊃UNBOUND(B)∨UNBOUND(C)
(label split_unbound)

(define bound |∀a.bound(a)=min(λxv.a⊂segm(xv))|)

(trw |∀a.natnum(bound(a))| (open bound))
;∀A.NATNUM(BOUND(A))
(label simpinfo) (label boundsort)

(trw |∀a.(¬unbound(a))≡a⊂segm(bound(a))|
     (open bound unbound) (use minprop2 mode: exact ue: ((a . |λxv.a⊂segm(xv)|))))
;∀A.¬UNBOUND(A)≡A⊂SEGM(BOUND(A))
(label boundfact)
(save-proofs natset)